Step of Proof: nat_ind 12,41
Inference at * 1 0 1 3 1 2 1 
Iof proof for Lemma nat ind:

.....upcase..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. j : 
5. 0 < j
6. P(j - 1)
  P(j) 
latex
 by Id  
latex

 1: .....upcase..... NILNIL

 1:   P(j)
 .

origin